$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$, $y$, $z$:$T$. ($x$ = $f$($y$)) $\Rightarrow$ ($\neg$($x$ = $y$)) $\Rightarrow$ $y$ is $f$$\ast$($z$) $\Rightarrow$ ($R$($y$,$z$) $\vee$ ($y$ = $z$)) $\Rightarrow$ $R$($x$,$z$))
\\[0ex]$\Rightarrow$ \{$\forall$$x$, $y$:$T$. $x$ = $f$+($y$) $\Rightarrow$ $R$($x$,$y$)\}